#pragma once

#include <bdd.h>
#include <bits/stdc++.h>
#include <common/define.h>
#include <sylvan_obj.hpp>
#include <mutex>

#ifdef USE_NANOBDD
#include <nanobdd/Nanobdd.h>
#include <execution>
#include <numeric>
#endif

#ifdef USE_NANOBDD_PRO
#include <nanobdd/nanobdd.h>
#include <execution>
#include <numeric>
#endif

namespace flashpp {

#ifdef USE_MTBDD
using namespace sylvan;

class HeaderSpace {
 public:
  HeaderSpace() {
    pred_ = sylvan::Bdd::bddZero();
  }

  HeaderSpace(sylvan::Bdd bdd) {
    pred_ = bdd;
  }

  static std::mutex locker;

  auto
  pred() const {
    return pred_;
  }

  bool
  isFalse() {
    return pred_.isZero();
  }

  bool
  isTrue() {
    return pred_.isOne();
  }

  HeaderSpace
  operator&(const HeaderSpace& hs) const {
    return HeaderSpace(pred_ & hs.pred());
  }

  HeaderSpace
  operator|(const HeaderSpace& hs) const {
    return HeaderSpace(pred_ | hs.pred());
  }

  HeaderSpace
  operator-(const HeaderSpace& hs) const {
    return HeaderSpace(pred_ & !hs.pred());
  }

  HeaderSpace
  operator!() const {
    return HeaderSpace(!pred_);
  }

  bool
  operator==(const HeaderSpace& hs) const {
    return pred_ == hs.pred();
  };

  bool
  operator!=(const HeaderSpace& hs) const {
    return pred_ != hs.pred();
  };

  bool
  operator<(const HeaderSpace& hs) const {
    return (pred_ < hs.pred());
  }

  static HeaderSpace
  fromInt(uint32_t addr, int prefixLength) {
    auto result = sylvan::Bdd::bddOne();
    std::bitset<32> bits(addr);

    for (int i = 31; i > (31 - prefixLength); i--) {
      if (bits.test(i)) {
        result = result * vars[31 - i];
      } else {
        result = result * (!vars[31 - i]);
      }
    }

    return HeaderSpace(result);
  }

  static HeaderSpace
  orAll(const std::set<HeaderSpace> hss) {
    auto r = sylvan::Bdd::bddZero();
    for (auto& h : hss) {
      r = r + h.pred();
    }
    return HeaderSpace(std::move(r));
  }

  static std::vector<sylvan::Bdd> vars;

 private:
  sylvan::Bdd pred_;
};
#endif

#ifdef USE_BDD

class HeaderSpace {
 public:
  HeaderSpace() {
    pred_ = bdd_false();
  }
  HeaderSpace(bdd pred) {
    pred_ = pred;
  };

  static std::mutex locker;

  bdd
  pred() const {
    return pred_;
  }

  bool
  isFalse() {
    return pred_ == bdd_false();
  }

  bool
  isTrue() {
    return pred_ == bdd_true();
  }

  static HeaderSpace fromInt(uint32_t&& addr, int& prefixLength);

  // Convert IP/msk to HS
  static HeaderSpace fromString(std::string addr);
  std::string serialize();
  static HeaderSpace deserialize(std::string data);

  HeaderSpace operator&(const HeaderSpace& hs) const;
  HeaderSpace operator|(const HeaderSpace& hs) const;
  HeaderSpace operator!() const;
  bool operator==(const HeaderSpace& hs) const;
  bool operator!=(const HeaderSpace& hs) const;
  HeaderSpace
  operator-(const HeaderSpace& hs) const {
    locker.lock();
    auto r = HeaderSpace(std::move(pred_ & !hs.pred()));
    locker.unlock();
    return r;
  }
  static HeaderSpace
  andAll(const std::set<HeaderSpace> hss) {
    auto r = bdd_true();
    locker.lock();
    for (auto& h : hss) {
      r = r & h.pred();
    }
    locker.unlock();
    return HeaderSpace(std::move(r));
  }
  static HeaderSpace
  orAll(const std::set<HeaderSpace> hss) {
    auto r = bdd_false();
    locker.lock();
    for (auto& h : hss) {
      r = r | h.pred();
    }
    locker.unlock();
    return HeaderSpace(std::move(r));
  }

  bool
  operator<(const HeaderSpace& hs) const {
    return (pred_.id() < hs.pred().id());
  }

 private:
  bdd pred_;
};

#endif

#ifdef USE_NANOBDD
static std::mutex locker;
class HeaderSpace {
 public:
  HeaderSpace() : pred_(nanobdd::Nanobdd::falseNode) {}

  HeaderSpace(int trueOrFalse) {
    if (trueOrFalse) {
      pred_ = nanobdd::Nanobdd::trueNode;
    } else {
      pred_ = nanobdd::Nanobdd::falseNode;
    }
  }

  HeaderSpace(nanobdd::Bdd bdd) {
    pred_ = bdd;
  }

  HeaderSpace&
  operator=(HeaderSpace h) {
    pred_ = h.pred_;
    return *this;
  }

  static std::mutex locker;

  auto&
  pred() const {
    return pred_;
  }

  bool
  isFalse() {
    return pred_.isFalse();
  }

  bool
  isTrue() {
    return pred_.isTrue();
  }

  HeaderSpace
  operator&(const HeaderSpace& hs) const {
    // locker.lock();
    auto r = nbdd.bddAnd(pred_, hs.pred());
    // locker.unlock();
    return r;
  }

  HeaderSpace
  operator|(const HeaderSpace& hs) const {
    // locker.lock();
    auto r = nbdd.bddOr(pred_, hs.pred());
    // locker.unlock();
    return r;
  }

  HeaderSpace&
  operator|=(const HeaderSpace& hs) {
    // locker.lock();
    pred_ = nbdd.bddOr(pred_, hs.pred());
    // locker.unlock();
    return *this;
  }

  HeaderSpace
  operator-(const HeaderSpace& hs) const {
    // locker.lock();
    // auto r = nbdd.bddAnd(pred_, nbdd.bddNot(hs.pred()));
    auto r = nbdd.bddDiff(pred_, hs.pred());
    // locker.unlock();
    return r;
  }

  HeaderSpace&
  operator-=(const HeaderSpace& hs) {
    // locker.lock();
    // auto r = nbdd.bddAnd(pred_, nbdd.bddNot(hs.pred()));
    pred_ = nbdd.bddDiff(pred_, hs.pred());
    // locker.unlock();
    return *this;
  }

  HeaderSpace
  operator!() const {
    // locker.lock();
    auto r = nbdd.bddNot(pred_);
    // locker.unlock();
    return r;
  }

  bool
  operator==(const HeaderSpace& hs) const {
    return pred_ == hs.pred();
  };

  bool
  operator!=(const HeaderSpace& hs) const {
    return pred_ != hs.pred();
  };

  bool
  operator<(const HeaderSpace& hs) const {
    return (pred_ < hs.pred());
  }

  static HeaderSpace
  fromInt(std::bitset<32>& bits, int prefixLength) {
    nanobdd::Bdd result = nanobdd::Nanobdd::trueNode;
    // std::bitset<32> bits(addr);

    std::vector<nanobdd::Bdd> bdds;
    for (int i = 31; i > (31 - prefixLength); i--) {
      if (bits.test(i)) {
        bdds.push_back(nbdd.getVar(31 - i));
      } else {
        bdds.push_back(nbdd.getNvar(31 - i));
      }
    }

    return std::reduce(
        std::execution::par_unseq,
        bdds.begin(),
        bdds.end(),
        result,
        [](auto x, auto y) { return nbdd.bddAnd(x, y); });

    // for (int i = 31; i > (31 - prefixLength); i--) {
    //   if (bits.test(i)) {
    //     result = nbdd.bddAnd(result, nbdd.getVar(31 - i));
    //   } else {
    //     result = nbdd.bddAnd(result, nbdd.bddNot(nbdd.getVar(31 - i)));
    //   }
    // }

    // return HeaderSpace(result);
  }

  static HeaderSpace
  orAll(const std::set<HeaderSpace> hss) {
    nanobdd::Bdd r = nanobdd::Nanobdd::falseNode;
    for (auto& h : hss) {
      r = nbdd.bddOr(r, h.pred());
    }
    return HeaderSpace(std::move(r));
  }
  // prime 999983
  static inline nanobdd::Nanobdd nbdd = nanobdd::Nanobdd(999983, 100, 10000000);

 private:
  nanobdd::Bdd pred_;
};
#endif

#ifdef USE_NANOBDD_PRO
class HeaderSpace : public nanobdd::Bdd {
 public:
  HeaderSpace() : nanobdd::Bdd() {}

  HeaderSpace(nanobdd::Bdd bdd) {
    root_ = bdd.root();
  }

  static HeaderSpace
  hsAll() {
    return nanobdd::bddTrue();
  }

  static HeaderSpace
  hsEmpty() {
    return nanobdd::bddFalse();
  }

  static HeaderSpace
  fromInt(std::bitset<32>& bits, int prefixLength) {
    nanobdd::Bdd result = nanobdd::bddTrue();
    // std::bitset<32> bits(addr);

    std::vector<nanobdd::Bdd> bdds;
    for (int i = 31; i > (31 - prefixLength); i--) {
      if (bits.test(i)) {
        bdds.push_back(nanobdd::getVar(31 - i));
      } else {
        bdds.push_back(nanobdd::getNvar(31 - i));
      }
    }

    return std::reduce(
        std::execution::par_unseq,
        bdds.begin(),
        bdds.end(),
        result,
        [](auto x, auto y) { return x & y; });
  }
};
#endif

} // namespace flashpp